package org.korifey.ffbdd.impl;

import java.io.IOException;
import java.util.ArrayList;

import org.korifey.ffbdd.api.IBddBackend;
import org.korifey.ffbdd.api.INode;
import org.korifey.ffbdd.api.INonterminal;
import org.korifey.ffbdd.api.ITerminal;

import static org.korifey.ffbdd.common.util.ByteUtil.*;

public class BddBackendBitvector implements IBddBackend {
	
	public static final int BYTES_PER_NODE = 9;
	
	protected int maxnonterminals;
	protected int maxterminals;
	
	protected byte[] ntMain;  // array of blocks [ 9 byte = 15 bit(var) + 1 bit (mark, var-sign)  + 3 byte(one-index) + 3 byte(zero-index) + 4bit (one-index-tail) + 4bit (zero-index-tail)]
	protected ITerminal<?>[] terminals;
	
	protected int nTerms;
	protected int nNterms;
	
	public BddBackendBitvector() {		
	}
	
	public void init(int maxnonterminals, int maxterminals) {
		if (maxnonterminals<0 || maxnonterminals > BitvectorConst.MAXNONTERMINALS)
			throw new IllegalArgumentException("'maxnonterminals' must be between 0 and " +
					BitvectorConst.MAXNONTERMINALS+ " inclusively, while now it is "+maxnonterminals);
		if (maxterminals<0 || maxterminals > BitvectorConst.MAXTERMINALS)
			throw new IllegalArgumentException("'maxterminals' must be between 0 and " +
					BitvectorConst.MAXTERMINALS+ " inclusively, while now it is "+maxterminals);
		
		this.maxnonterminals = maxnonterminals;
		this.maxterminals = maxterminals;		
		ntMain = new byte[maxnonterminals * BYTES_PER_NODE];		
		terminals = new ITerminal[maxterminals];
		nTerms = 0;
		nNterms = 0;
	}
	
	public INode getNode(int index) {
		if (index < 0) return terminals[-index - 1];
		else {
			int idx = index * BYTES_PER_NODE;
			int var = twoByteToInt(ntMain[idx], ntMain[idx + 1]);
			boolean mark = BitvectorConst.isMarked(var);
			var = BitvectorConst.realVar(var);
			
			//var = 0 means no node at current index
			if (var == 0) return null;			
			int one = threeByteAndHalfToInt(
					ntMain[idx + 2], ntMain[idx + 3], ntMain[idx + 4], 
					halfByteToInt(ntMain[idx+8], true));
			int zero = threeByteAndHalfToInt(
					ntMain[idx + 5], ntMain[idx + 6], ntMain[idx + 7], 
					halfByteToInt(ntMain[idx+8], false));
			NonterminalImpl res = new NonterminalImpl(var, BitvectorConst.realIndex(one), BitvectorConst.realIndex(zero), this, index);
			res.mark = mark; //no setMark, because it's set already
			return res;
		}
	}
	
	
	
	public INode insertNonterminal(int var, INode one, INode zero) {				
		NodeImpl _one = (NodeImpl)one;
		NodeImpl _zero = (NodeImpl)zero;
		if (_one.getIndex() == _zero.getIndex()) return one;
		
		NonterminalImpl nt = new NonterminalImpl(var, _one.getIndex(), _zero.getIndex(), this);
		
		int n = maxnonterminals;
		int h1 = nt.hashCode() % n;
		if (h1 < 0) h1 = n + h1;
		int h2 = (nt.hashCode()*13 + 37) % n;
		if (h2 < 0) h2 = n + h2;
		if (h2 == 0) h2 = 1;
		
		for (INonterminal t = (INonterminal)getNode(h1); t!= null; h1 = (h1 + h2) % n, t = (INonterminal)getNode(h1)) {
			if (nt.equals(t)) return t;
		}
		nt.setIndex(h1);
		nNterms++;
		if (nNterms >= maxnonterminals*0.75) throw new RuntimeException("Limit of nonterminals reached");
		putNterm(nt);
		return nt;
	}

	
	
	public <E> ITerminal<E> insertTerminal(E value) {		
		int n = maxterminals;
		TerminalImpl<E> tt = new TerminalImpl(value);
		int h1 = (tt.hashCode()) % n;
		if (h1 < 0) h1 = n + h1;
		int h2 = (tt.hashCode()*13 + 37) % n;
		if (h2 < 0) h2 = n + h2;
		if (h2 == 0) h2 = 1;
				
		for (ITerminal<?> t = terminals[h1]; t!= null; h1 = (h1 + h2) % n, t = terminals[h1]) {			
			if (tt.equals(t)) return (ITerminal<E>)t;
		}
		
		tt.setIndex(-h1 - 1);
		nTerms ++;
		if (nTerms >= maxterminals*0.75) throw new RuntimeException("Limit of terminals reached");
		terminals[h1] = tt;
		return tt;
	}
	
	
	private void putNterm(NonterminalImpl nt) {
		int idx = nt.getIndex()* BYTES_PER_NODE;		
		intToTwoBytes(nt.var(), ntMain, idx);
		int remHi = intToThreeBytesAndHalf(BitvectorConst.fakeIndex(nt.oneIndex()), ntMain, idx+2);
		int remLo = intToThreeBytesAndHalf(BitvectorConst.fakeIndex(nt.zeroIndex()), ntMain, idx+5);
		ntMain[idx+8] = twoHalfsToByte(remHi, remLo);
	}

	@Override
	public void gc() {
		//TODO implement
	}

	@Override
	public int getMaxNonterminals() {
		return maxnonterminals;
	}

	@Override
	public int getMaxTerminals() {
		return maxterminals;
	}

	@Override
	public int getNonterminalsNumber() {
		return nNterms;
	}

	@Override
	public int getTerminalsNumber() {
		return nTerms;
	}

	@Override
	public void setMark(int index, boolean mark) {
		int idx = index * BYTES_PER_NODE;
		int fakeVar = twoByteToInt(ntMain[idx], ntMain[idx + 1]);
		int realVar = BitvectorConst.realVar(fakeVar);
		fakeVar = BitvectorConst.makeFakeVar(realVar, mark);
		intToTwoBytes(fakeVar, ntMain, idx);
	}
	
}
